An integrated circuit is not typically implemented in hardware (e.g. silicon) until the hardware design for the integrated circuit is verified because post-silicon error discovery can be costly.
As is known to those of skill in the art there are several methods for verifying a hardware design including simulation based verification (also referred to as dynamic verification) and formal verification. The main difference between simulation based verification and formal verification is that simulation based verification is input-based (e.g. the test engineer supplies the test input signals) and formal verification is output-based (e.g. the test engineer provides the output properties to be verified).
In formal verification, the hardware design is transformed into a mathematical model (e.g. a state-transition system) and the properties to be verified are expressed using mathematical logic using a precise syntax or a language with a precise mathematical syntax and semantics. A property is then verified by searching the entire reachable state space of the hardware design without explicitly traversing the state machine. Since formal verification algorithmically and exhaustively explores all input values over time, verifying properties in this manner allows a property to be exhaustively proved or disproved for all states.
Many integrated circuits, such as system-on-chips (SoCs) implement one or more counters. Accordingly, verifying such hardware designs includes verifying the operation of the counter(s) in the hardware design. However, when the counter is large (e.g. sixteen bits or more) exhaustive verification through simulation-based verification or known formal verification methods becomes infeasible due to the large number of possible combinations.
The embodiments described below are provided by way of example only and are not limiting of implementations which solve any or all of the disadvantages of known methods for verifying the operation of a counter in a hardware design.